COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.REQUIRE "LSP.PUB[206,CLT]" source_file
C00003 00003	.hd206 FALL 1977
C00005 ENDMK
C⊗;
.REQUIRE "LSP.PUB[206,CLT]" source_file;
.PAGE FRAME 56 HIGH 80 WIDE;
.evenleftborder ← oddleftborder ← 1000;
.area text lines 1 to 56;
.place text;
.
.MACRO  hd206 (TERM) ⊂
.BEGIN    NOFILL  TURNON "←→"
←COMPUTER SCIENCE DEPARTMENT
←STANFORD UNIVERSITY
.SKIP  
CS206  ←COMPUTING WITH SYMBOLIC EXPRESSIONS  →TERM
.TURNOFF
.END ⊃
.
.
.MACRO hw (NUMBER, DUEDATE) ⊂
.   BEGIN TURNON "←"  NOFILL
←PROBLEM SET  NUMBER
←Due  DUEDATE
.   TURNOFF END ⊃
.
.itemmac
.
.PORTION MAINPORTION
.
.hd206 FALL 1977
.skip
.hw 2, |November 3|
.
.bb General comments. 


	This assignment involves proving properties of LISP functions.  
Unless otherwise noted your proofs should be fairly formal.  
The level of detail should be approximately
that of Chapter_III section_7 of the notes.  
For each step of your proof, make sure that 
you list all of the facts (axioms, earlier steps or previously proved properties)
that are necessary to make that step.  
You may use any properties already proved in the notes or in class.

.item←0
.begin   indent 0,6
.bb Assignment.

#. Chapter III.  Exercise 1. ii-v.

#. Chapter III.  Exercise 2. 

#. Let ⊗andlist be as defined in Chapter I and assume ⊗p is a suitably well-behaved
predicate.  Prove the following:

	##. ⊗⊗∀u v: [andlis[u*v, p] = andlis[u, p] ∧ andlis[v, p]]⊗

	##. ⊗⊗∀u: [andlis[reverse u, p] = andlis[u, p]]⊗

Hint: you will need to phrase this problem in terms of extended truth values (ETV)
and state axioms relating this problem to the restatement.  
.end